Theorem vtoclbg 3240

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 334	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3239	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175

This theorem is referenced by:  alexeqg  3302  pm13.183  3313  sbc8g  3410  sbc2or  3411  sbcco  3425  sbc5  3427  sbcie2g  3436  eqsbc3  3442  sbcng  3443  sbcimg  3444  sbcan  3445  sbcor  3446  sbcbig  3447  sbcal  3452  sbcex2  3453  sbcel1v  3462  sbcreu  3482  csbiebg  3522  sbcel12  3935  sbceqg  3936  elpwg  4116  snssg  4268  preq12bg  4326  elintgOLD  4419  elintrabg  4424  sbcbr123  4636  opelresg  5324  inisegn0  5416  funfvima3  6399  elixpsn  7833  ixpsnf1o  7834  domeng  7855  1sdom  8048  rankcf  9478  eldm3  30905  br1steqg  30919  br2ndeqg  30920  elima4  30924  brsset  31166  brbigcup  31175  elfix2  31181  elfunsg  31193  elsingles  31195  funpartlem  31219  ellines  31429  elhf2g  31453  cover2g  32679  sbcrexgOLD  36367  sbcangOLD  37760  sbcorgOLD  37761  sbcalgOLD  37773  sbcexgOLD  37774  sbcel12gOLD  37775  sbcel1gvOLD  38116