Theorem vtoclbg 3267

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 335	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3266	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  alexeqg  3332  pm13.183  3344  sbc8g  3443  sbc2or  3444  sbcco  3458  sbc5  3460  sbcie2g  3469  eqsbc3  3475  sbcng  3476  sbcimg  3477  sbcan  3478  sbcor  3479  sbcbig  3480  sbcal  3485  sbcex2  3486  sbcel1v  3495  sbcreu  3515  csbiebg  3556  sbcel12  3983  sbceqg  3984  elpwg  4166  snssg  4327  preq12bg  4386  elintgOLD  4484  elintrabg  4489  sbcbr123  4706  opelresg  5404  inisegn0  5497  funfvima3  6495  elixpsn  7947  ixpsnf1o  7948  domeng  7969  1sdom  8163  rankcf  9599  eldm3  31651  br1steqgOLD  31674  br2ndeqgOLD  31675  elima4  31679  brsset  31996  brbigcup  32005  elfix2  32011  elfunsg  32023  elsingles  32025  funpartlem  32049  ellines  32259  elhf2g  32283  cover2g  33509  sbcrexgOLD  37349  sbcangOLD  38739  sbcorgOLD  38740  sbcalgOLD  38752  sbcexgOLD  38753  sbcel12gOLD  38754  sbcel1gvOLD  39094