Theorem vtoclbg 3557

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-clel 2816

This theorem is referenced by:  alexeqg  3651  pm13.183  3666  elab6g  3669  elabgw  3677  sbc8g  3796  sbc2or  3797  sbccow  3811  sbcco  3814  sbc5ALT  3817  sbcie2g  3829  eqsbc1  3835  sbcng  3836  sbcimg  3837  sbcan  3838  sbcor  3839  sbcbig  3840  sbcal  3849  sbcex2  3850  sbcel1v  3856  sbcreu  3876  csbiebg  3931  sbcel12  4411  sbceqg  4412  csbie2df  4443  preq12bg  4853  elintrabg  4961  sbcbr123  5197  inisegn0  6116  fsn2g  7158  funfvima3  7256  elixpsn  8977  ixpsnf1o  8978  domeng  9003  1sdomOLD  9285  rankcf  10817  eldm3  35761  elima4  35776  brsset  35890  brbigcup  35899  elfix2  35905  elfunsg  35917  elsingles  35919  funpartlem  35943  ellines  36153  elhf2g  36177  bj-elpwgALT  37055  cover2g  37723  sbcrexgOLD  42796